perm filename FR.BNF[BNF,JRA] blob
sn#045421 filedate 1973-05-24 generic text, type T, neo UTF8
00100 <AXIOM> ::=<NAME><ASSUM><DRECUR><INEQ><BODY>
00200 =>[(PROG(LSTNAME)
00205 (SETQ LSTNAME(READLIST(APPEND LST(EXPLODE(STK4)))))
00210 (RETURN (LIST (QUOTE DEFPROP)(STK4)
00220 (CONS (QUOTE THCONSE)
00230 (CONS
00235 (APPEND(UNION POSTLIST PRELIST)(LIST (QUOTE CGL)(LIST LSTNAME(LIST (QUOTE QUOTE) POSTLIST))))
00240 ( APPEND(CDR (STK0))
00250 (QUOTE((THSETQ(THV LCTR)(THV GCTR))))
00260 (COND((NULL(STK2))(LIST(LIST (QUOTE THUNIQUE) LSTNAME))))
00270 (LIST(LIST(QUOTE TREEPATH)(STK4)(CADR(STK0)))
00280 (QUOTE(TRACEINFO1))
00285 (LIST (QUOTE THOR) T(LIST(QUOTE TRACEINFO2)(STK4)))
00290 (QUOTE(COND((TTYIN)(ADVICESYS)))))
00292 (COND((EQ(CAAR(STK0))(QUOTE THAND))(CDAR(STK0)))(T(LIST(CAR(STK0)))))
00294 (QUOTE((THSETQ(THV DBLITS)(CONS(CDAR CT)(THV DBLITS)))
00296 (COND((EQ(QUOTE IF)(CADAR CT))(ELSECLAUSE))(T(THSETQ CT(CDR CT)T T))))))
00298 ))(QUOTE THEOREM))))]
00300 <NAME>::= <ID> =>[(PROG2(SETQ VARLIST(SETQ POSTLIST(SETQ PRELIST NIL)))(STK0))]
00400
00500 <ASSUM>::= T =>T
00600 ::=NIL => NIL
00700
00800 <DRECUR> ::= T =>T
00900 ::= NIL => NIL
01000
01100 <INEQ> ::= NIL =>NIL
01200 ::=(<INARGS> =>*
01300
01400 <INARGS> ::= <INARG>,<INARGS> =>(INARG . INARGS)
01500 ::= <INARG>) =>(INARG)
01600
01700 <INARG> ::= X =>X
01800 ::= ⊗ =>⊗
01900
02000 <BODY> ::= <PRECONDS><POSTCOND> =>[(PROG2(SETQ POSTLIST VARLIST)(CONS(STK1)(STK0)))]
02005 <PRECONDS> ::= <PC>; =>[(PROG NIL(SETQ PRELIST VARLIST)(SETQ VARLIST NIL)(RETURN(STK1)))]
02010
02015 <PC> ::= <C1><PCL> =>[(CONS (QUOTE THAND)(CONS (STK1)(STK0)))]
02020 ::= <C1>=>*
02025
02030 <PCL> ::= <C1><PCL> =>(C1 .PCL)
02035 ::= <C1> =>(C1)
02040
02045 <C1> ::= <C> ; => C
02050
02055 <C> ::= <PRED> <CL> =>[(APPEND(CONS (QUOTE THOR)(CONS(STK1)(STK0)))(QUOTE((CONDSTAT(THV GCL)T))))]
02060 ::= <PRED> =>*
02065 ::= (<PC>) =>*
02070
02075 <CL> ::= <PRED><CL> =>(PRED .CL)
02080 ::= <PRED> =>(PRED)
02085 ::=(<PC>) =>(PC)
02090
02700 <PRED> ::= <NOT> <LIT> =>[(COND((EQ(CAR(STK0))(QUOTE =))(MAKEQUAL(CDR(STK0))(CONS(QUOTE EQUAL)(CDR STK0))))(T(MAKENOT(STK0))))]
02750
02800 ::= <LIT> =>[(COND((EQ(CAR(STK0))(QUOTE =))(MAKEQUAL(CDR(STK0))
02850 (LIST(QUOTE NOT)(CONS(QUOTE EQUAL)(CDR(STK0))))))(T(MAKEPRED(STK0))))]
02875
02900
03000 <LIT> ::= <PREDLET><ITMLST> =>(PREDLET . ITMLST)
03100
03200 <ITMLST> ::= (<ITMS> =>*
03300
03400 <ITMS> ::= <TM2><ITMS> =>(TM2 . ITMS)
03500 ::= <TM>) =>(TM)
03600
03700 <TM2> ::= <TM>, =>*
03800
03900 <TM> ::= <IVAR> =>[(PROG2(COND((NOT(MEMQ(STK0)VARLIST))(SETQ VARLIST(CONS(STK0)VARLIST))))
03950 (LIST (QUOTE THV)(STK0)))]
04000 ::=<PREFN><ITMLST> =>(PREFN . ITMLST)
04100 ::= <PREFN> =>(PREFN)
04200
04300 <POSTCOND> ::= <POSTPRED>;<POSTCOND> =>(POSTPRED . POSTCOND)
04400 ::= ;=>NIL
04500 <POSTPRED> ::= <NOT><LIT> => (NOT . LIT)
04550 ::= <LIT> => *
04600
06000 <IVAR> ::= <ID> =>*
06100 <PREFN> ::= <ID> =>*
06200 <PREDLET> ::= <ID> =>*
06250 ::= = => =
06300
06350 <NOT> ::= ¬ => ¬
06400 END